Nuprl Lemma : qadd_functionality_wrt_qle
11,40
postcript
pdf
a
,
b
,
c
,
d
:
.
a
b
c
d
a
+
c
b
+
d
latex
Definitions
P
&
Q
,
T
,
P
Q
,
P
Q
,
,
True
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
qadd
wf
,
qle
transitivity
qorder
,
qadd
com
,
true
wf
,
squash
wf
,
grp
op
preserves
le
qorder
,
rationals
wf
,
qle
wf
origin
a, b, c, d:
. a 
b 
c d a + c b + d a, b, c, d:. a b c d a + c b + d 
T
Q Q
T Qx:A. B(x)